T1, T2:Type, f:(T1T2), Q:(T2), L:T1 List.
filter(Q;map(f;L)) = map(f;filter(Q o f;L))  T2 List 

latex

Definitions	x:A. B(x), b, t  T, A, b, Prop, , P  Q, P & Q, P  Q, Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf